Require Import Rdefinitions.
Require Import MathClasses.interfaces.abstract_algebra.

Class CarrierBDefs (CarrierB : Type) : Type :=
  {
    CarrierBz : CarrierB;
    CarrierBe :> Equiv CarrierB;
    CarrierBE :> Equivalence CarrierBe
  }.

Module Type CType.
  Parameter t : Type.
  Parameter CTypeZ : t.
  Declare Instance CTypeEquiv : Equiv t.
  Declare Instance CTypeEquivalence : Equivalence CTypeEquiv.
End CType.

(* SigmaHCOL model *)
Section Sigma.
  (* CarrierB : Type is implicitly defined. We can also
     define it explicitly in this section. *)
  Context `{CBDEFS : CarrierBDefs}.

  Lemma sym_test :
    forall b1 b2 : CarrierB,
      CarrierBe b1 b2 <-> CarrierBe b2 b1.
  Proof.
    now symmetry.
  Qed.

  Definition DynWin_SHCOL := CarrierBz.
  
End Sigma.

(* MHCOL/DHCOL model
   Note: this is currently closer to DHCOL, but in reality the transition needs
   to happen at SHCOL->MHCOL step.
*)
Module Type DHCOL (CT : CType).

  Inductive operator := const_op : CT.t -> operator.

End DHCOL.

Module AHCOL (CT : CType) <: DHCOL(CT).

  Include DHCOL CT.

  Instance CTasCarrierB : CarrierBDefs CT.t :=
    {
      CarrierBz := CT.CTypeZ;
      CarrierBe := CT.CTypeEquiv;
      CarrierBE := CT.CTypeEquivalence;
    }.

  Lemma sym_test' :
    forall b1 b2 : CT.t,
      CT.CTypeEquiv b1 b2 <-> CT.CTypeEquiv b2 b1.
  Proof.
    pose proof sym_test.
    intros.
    unfold CarrierBe, CTasCarrierB in *.
    eapply H.
  Qed.

End AHCOL.

(* To be generated by MetaCoq (compilation) *)
Module DynWin_AHCOL_MetaMod (CT:CType).

  Include AHCOL CT.
  Definition DynWin' := const_op CT.CTypeZ.
  
End DynWin_AHCOL_MetaMod.

Module DynWinProofs_Mod (CT:CType).

  (* Include AHCOL CT. *)
  Include DynWin_AHCOL_MetaMod CT.

  Lemma DynWin_correct : eq DynWin' (const_op DynWin_SHCOL).
  Proof.
    reflexivity.
  Qed.
  
End DynWinProofs_Mod.

(* *)

(* Proofs the old way:
   1) (CarrierBasCT)
   2) Instantiate AHCOL
   3) Open section with CarrierBDefs instance and AHCOL import
   4) Proof inside section

   Translation old way
   1) MetaCoq

   Proofs the new way:
   1) Move proofs from old section into AHCOL

   Translation the new way:
   1) MetaCoq [is the same?]
*)

Instance R_CarrierB : CarrierBDefs R :=
  {
    CarrierBz := R0;
    CarrierBe := eq;
    CarrierBE := eq_equivalence;
  }.


Section DynWinProofs.
  Parameter CarrierB: Type. (* proving forall types as CarrierB *)
  Context {CADEFS: CarrierBDefs CarrierB}. (* as long as it satisfies CarrierBDefs *)

  Fail Lemma S_to_A: DynWin_SHCOL = DynWin'.


End DynWinProofs.
